es:ES, e:E, x:Id. state after e\\x  state@loc(e)\\x 

latex

Definitions	x:A. B(x), t  T, state@i\\x, state after e\\x, if b t else f fi, Top, P  Q, true, Prop, false, , Unit, P  Q, P & Q,
Lemmas	eq id wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert-eq-id, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, es-after wf, Id wf, es-E wf, event system wf